타입에 대한 내재적 관점과 외재적 관점
내재적(intrinsic) 관점과 외재적(extrinsic) 관점은 타입 이론에서 타입을 보는 두가지 관점이다.
내재적 관점은 "intrinsically typed", "처치 스타일(types à la Church)", "타입 검사 시스템(type checking system)", 외재적 관점은 "extrinsically typed", "커리 스타일(types à la Curry)", "타입 할당 시스템(type assignment system)" 등으로 불린다 [2, chap. DeBruijn, 1:8–9].
예시 : 단순 타입 λ-계산
단순 타입 λ-계산의 타입 시스템은 다음과 같이 두가지 방식으로 제시 될 수 있다.
내재적 시스템
\[ \begin{array}{ll} A, B &::= A \to B \mid \ldots \\ M, N &::= \lambda x:A. M \mid M \ N \end{array} \] \[ \begin{prooftree} \AXC{$\Gamma , x:A \vdash M : B$} \UIC{$\Gamma \vdash \lambda x:A. M : A \to B$} \end{prooftree} \quad \begin{prooftree} \AXC{$\Gamma \vdash M : A \to B$} \AXC{$\Gamma \vdash N : A$} \BIC{$\Gamma \vdash M \ N : B$} \end{prooftree} \]
외재적 시스템
\[ \begin{array}{ll} A, B &::= A \to B \mid \ldots \\ M, N &::= \lambda x. M \mid M \ N \end{array} \] \[ \begin{prooftree} \AXC{$\Gamma , x:A \vdash M : B$} \UIC{$\Gamma \vdash \lambda x. M : A \to B$} \end{prooftree} \quad \begin{prooftree} \AXC{$\Gamma \vdash M : A \to B$} \AXC{$\Gamma \vdash N : A$} \BIC{$\Gamma \vdash M \ N : B$} \end{prooftree} \]
타입 유일성
내재적 시스템에서는 타입의 유일성이 성립한다.
If \(\Gamma \vdash M : A\) and \(\Gamma \vdash M : B\), then \(A = B\)
외재적 시스템에서는 이러한 타입의 유일성이 성립하지 않는다.